CMake build system: support system-provided MiniSat #7644

tautschnig · 2023-04-03T12:10:41Z

Some operating systems provide packaged versions of MiniSat. When building distribution packages it may then be preferable to use the pre-installed library instead of building the solver object from scratch. With this patch it is now possible to select "system-minisat2" as a solver, alongside any other solvers that may be built from scratch.

Each commit message has a non-empty body, explaining why the change was made.
n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

codecov · 2023-04-03T13:06:52Z

Codecov Report

Patch coverage has no change and project coverage change: -0.35 ⚠️

Comparison is base (453eb65) 78.55% compared to head (d8646ca) 78.21%.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7644      +/-   ##
===========================================
- Coverage    78.55%   78.21%   -0.35%     
===========================================
  Files         1691     1691              
  Lines       193125   193125              
===========================================
- Hits        151712   151051     -661     
- Misses       41413    42074     +661

see 43 files with indirect coverage changes

☔ View full report in Codecov by Sentry.
📢 Do you have feedback about the report comment? Let us know in this issue.

esteffin · 2023-04-03T15:46:57Z

src/solvers/CMakeLists.txt

@@ -87,6 +87,15 @@ foreach(SOLVER ${sat_impl})
        target_sources(solvers PRIVATE ${minisat2_source})

        target_link_libraries(solvers minisat2-condensed)
+    elseif("${SOLVER}" STREQUAL "system-minisat2")
+        include(CheckIncludeFileCXX)
+        CHECK_INCLUDE_FILE_CXX("minisat/simp/SimpSolver.h" minisat_header_found)


💡 From CMake 3.12 CHECK_INCLUDE_FILE_CXX can also check the existence of a counterpart library component by using CMAKE_REQUIRED_LIBRARIES.
It may be worth increasing the minimum cmake required version and check for the library as well.

Moving beyond 3.10 would mean CBMC no longer builds (with CMake) on Ubuntu 18.04. Perhaps not a very strong argument as that is long deprecated, but still. So for now I've just added a comment reflecting what you educated me about.

Moving beyond 3.10 would mean CBMC no longer builds (with CMake) on Ubuntu 18.04. Perhaps not a very strong argument as that is long deprecated, but still. So for now I've just added a comment reflecting what you educated me about.

I'd like to keep build on Ubuntu 18.04 alive for a little bit longer -- this is/was an incredibly popular choice, not least for university academics, but well beyond that.

It may be worth noting that the Ubuntu 18.04 CI jobs were removed in this PR - #7657

The runners for github actions no longer support Ubuntu 18.04. So we had no straight forward way to keep the checks operational. It could potentially be done, but would require porting them over to docker. As such it is currently only a matter of time before issues are introduced which accidentally break the Ubuntu 18.04 build.

esteffin · 2023-04-03T15:50:19Z

The changes looks good to me.
Unfortunately this changes will not work with the Rust library as at the moment the Rust component expects a self-contained .a file with all the dependencies (including all sat solvers) bundled together.

@NlightNFotis We can specifically mark that using minisat2-system is not compatible with the Rust API?

NlightNFotis · 2023-04-28T16:57:42Z

Hello,

I have tried to build this branch locally and I have not been able to do so.

I have installed minisat through brew install minisat. I build with sat_impl set to system-minisat2, but it seems that it fails to find the header:

cmake -S. -Bbuild/ -Dsat_impl="system-minisat2" -DCMAKE_C_COMPILER=/usr/bin/clang -DCMAKE_CXX_COMPILER=/usr/bin/clang++
-- Building CBMC version 5.81.0
-- The C compiler identification is AppleClang 14.0.3.14030022
-- The CXX compiler identification is AppleClang 14.0.3.14030022
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Check for working C compiler: /usr/bin/clang - skipped
-- Detecting C compile features
-- Detecting C compile features - done
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Check for working CXX compiler: /usr/bin/clang++ - skipped
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Rule launch compile: /opt/homebrew/bin/ccache
-- Found BISON: /usr/bin/bison (found version "2.3") 
-- Found FLEX: /usr/bin/flex (found version "2.6.4") 
-- Found Doxygen: /opt/homebrew/bin/doxygen (found version "1.9.6") found components: doxygen dot 
-- Looking for C++ include minisat/simp/SimpSolver.h
-- Looking for C++ include minisat/simp/SimpSolver.h - not found
CMake Error at src/solvers/CMakeLists.txt:103 (message):
  Unable to find header file for preinstalled Minisat2

The error message comes from an addition of an else() block that displays the message:

if(${minisat_header_found})
    message(STATUS "Building solvers with minisat2 (pre-built)")
    target_compile_definitions(solvers PUBLIC SATCHECK_MINISAT2 HAVE_MINISAT2)
    target_sources(solvers PRIVATE ${minisat2_source})
    target_link_libraries(solvers minisat)
else()
    message(FATAL_ERROR "Unable to find header file for preinstalled Minisat2")
endif()

The confusing thing is that I do have it installed, and I can find the header file:

cbmc git:(5ce5e2e9b1) ✗ find `brew --prefix` | grep minisat/simp/SimpSolver.h
/opt/homebrew/Cellar/minisat/2.2.1/include/minisat/simp/SimpSolver.h

I have tried to get the directory in the list of included directories of CMake after some googling/stack-overflowing, but my CMake-fu is failing me.

This is what I ended up with but it doesn't seem to be working:

elseif("${SOLVER}" STREQUAL "system-minisat2")
   list(APPEND CMAKE_INCLUDE_PATH "/opt/homebrew/Cellar/minisat/2.2.1/include/")
   include(CheckIncludeFileCXX)
   set(CMAKE_REQUIRED_INCLUDES ${CMAKE_INCLUDE_PATH})
   # if/when we move to CMake 3.12 (or later) we could also check for the
   # library via CMAKE_REQUIRED_LIBRARIES
   CHECK_INCLUDE_FILE_CXX("minisat/simp/SimpSolver.h" minisat_header_found)
   if(${minisat_header_found})
       message(STATUS "Building solvers with minisat2 (pre-built)")
       target_compile_definitions(solvers PUBLIC SATCHECK_MINISAT2 HAVE_MINISAT2)
       target_sources(solvers PRIVATE ${minisat2_source})
       target_link_libraries(solvers minisat)
   else()
       message(FATAL_ERROR "Unable to find header file for preinstalled Minisat2")
   endif()
elseif("${SOLVER}" STREQUAL "glucose")

I was (crudely) trying to get the include path fixed, to get past compilation, but it didn't seem to be that responsive to my probes.

Any insight on how to get past this? @tautschnig

esteffin

Testing this with @NlightNFotis showed that when installing minisat with homebrew, CHECK_INCLUDE_FILE_CXX cannot find the header file.
It is also hard (I didn't find a way) to instruct CHECK_INCLUDE_FILE_CXX to look into a specific folder.

I would suggest to use a more robust mechanism to find an external dependency such as find_package. This will enable the user to specify additional folders to look into (as well as it will allow to check for the minisat library component as well as the header).

src/solvers/CMakeLists.txt

tautschnig · 2023-05-15T12:47:54Z

The changes looks good to me. Unfortunately this changes will not work with the Rust library as at the moment the Rust component expects a self-contained .a file with all the dependencies (including all sat solvers) bundled together.

@NlightNFotis We can specifically mark that using minisat2-system is not compatible with the Rust API?

The update version of this PR now includes a fix that will make sure also the minisat object files get included.

tautschnig · 2023-05-15T14:12:40Z

Package mirrors seem to be having a problem at this time: actions/runner-images#7596

tautschnig · 2023-05-15T14:15:22Z

Testing this with @NlightNFotis showed that when installing minisat with homebrew, CHECK_INCLUDE_FILE_CXX cannot find the header file. It is also hard (I didn't find a way) to instruct CHECK_INCLUDE_FILE_CXX to look into a specific folder.

I would suggest to use a more robust mechanism to find an external dependency such as find_package. This will enable the user to specify additional folders to look into (as well as it will allow to check for the minisat library component as well as the header).

I am now using find_path, which appears to solve the problem (according to my testing on macOS). Nevertheless, building against those files provided by brew won't work unless you silence warnings (fails with -Werror,-Wzero-length-array). So I'd claim the concerns have been addressed. @NlightNFotis @esteffin would you mind taking another look?

Some operating systems provide packaged versions of MiniSat. When building distribution packages it may then be preferable to use the pre-installed library instead of building the solver object from scratch. With this patch it is now possible to select "system-minisat2" as a solver, alongside any other solvers that may be built from scratch. The required support for external libraries also addresses diffblue#7641. Fixes: diffblue#7641

esteffin

I added a non-crucial comment, but as it is a solid improvement wrt the state of the art I will approve.

src/libcprover-cpp/CMakeLists.txt

esteffin · 2023-05-31T11:40:11Z

@tautschnig Regarding the failure on brew-provided minisat for now I would just add a mention that the mechanism is not working on Mac.

In the future it will be interesting to fix the problem as brew-provided minisat seems more recent than the apt one (unfortunately minisat does not provide a discoverable version).

tautschnig · 2023-05-31T12:00:53Z

@tautschnig Regarding the failure on brew-provided minisat for now I would just add a mention that the mechanism is not working on Mac.

In the future it will be interesting to fix the problem as brew-provided minisat seems more recent than the apt one (unfortunately minisat does not provide a discoverable version).

The fix here would be to either submit patches to homebrew or work around the problem by silencing some warnings via cmake command line compiler flags. The former is out of scope, the latter people interested in this can do locally?

Co-authored-by: Enrico Steffinlongo <[email protected]>

tautschnig requested a review from a team as a code owner April 3, 2023 12:10

esteffin reviewed Apr 3, 2023

View reviewed changes

tautschnig force-pushed the features/cmake-minisat-system branch from 93be70a to 5ce5e2e Compare April 18, 2023 10:27

tautschnig assigned NlightNFotis Apr 18, 2023

tautschnig self-assigned this May 2, 2023

esteffin suggested changes May 4, 2023

View reviewed changes

src/solvers/CMakeLists.txt Show resolved Hide resolved

tautschnig force-pushed the features/cmake-minisat-system branch from 5ce5e2e to e9d3f9b Compare May 15, 2023 13:59

tautschnig assigned esteffin and unassigned tautschnig May 15, 2023

tautschnig force-pushed the features/cmake-minisat-system branch from e9d3f9b to 3246c2b Compare May 31, 2023 11:26

tautschnig mentioned this pull request May 31, 2023

CMake error when building cbmc with -Dsat_impl=ipasir-cadical #7641

Closed

esteffin reviewed May 31, 2023

View reviewed changes

src/libcprover-cpp/CMakeLists.txt Show resolved Hide resolved

esteffin approved these changes May 31, 2023

View reviewed changes

Add warning message in case static library is missing

d8646ca

Co-authored-by: Enrico Steffinlongo <[email protected]>

tautschnig assigned tautschnig and unassigned NlightNFotis and esteffin May 31, 2023

tautschnig merged commit 0ca29d8 into diffblue:develop May 31, 2023

tautschnig deleted the features/cmake-minisat-system branch May 31, 2023 14:54

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

CMake build system: support system-provided MiniSat #7644

CMake build system: support system-provided MiniSat #7644

Uh oh!

tautschnig commented Apr 3, 2023

Uh oh!

codecov bot commented Apr 3, 2023 •

edited

Loading

Uh oh!

esteffin Apr 3, 2023

Uh oh!

tautschnig Apr 18, 2023

Uh oh!

kroening Apr 18, 2023

Uh oh!

thomasspriggs Apr 28, 2023

Uh oh!

esteffin commented Apr 3, 2023

Uh oh!

NlightNFotis commented Apr 28, 2023

Uh oh!

esteffin left a comment

Uh oh!

Uh oh!

tautschnig commented May 15, 2023

Uh oh!

tautschnig commented May 15, 2023

Uh oh!

tautschnig commented May 15, 2023

Uh oh!

esteffin left a comment

Uh oh!

Uh oh!

esteffin commented May 31, 2023

Uh oh!

tautschnig commented May 31, 2023

Uh oh!

Uh oh!

CMake build system: support system-provided MiniSat #7644

CMake build system: support system-provided MiniSat #7644

Uh oh!

Conversation

tautschnig commented Apr 3, 2023

Uh oh!

codecov bot commented Apr 3, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

esteffin Apr 3, 2023

Choose a reason for hiding this comment

Uh oh!

tautschnig Apr 18, 2023

Choose a reason for hiding this comment

Uh oh!

kroening Apr 18, 2023

Choose a reason for hiding this comment

Uh oh!

thomasspriggs Apr 28, 2023

Choose a reason for hiding this comment

Uh oh!

esteffin commented Apr 3, 2023

Uh oh!

NlightNFotis commented Apr 28, 2023

Uh oh!

esteffin left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

tautschnig commented May 15, 2023

Uh oh!

tautschnig commented May 15, 2023

Uh oh!

tautschnig commented May 15, 2023

Uh oh!

esteffin left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

esteffin commented May 31, 2023

Uh oh!

tautschnig commented May 31, 2023

Uh oh!

Uh oh!

codecov bot commented Apr 3, 2023 •

edited

Loading